A, B:Type, f:(A(B + Top)), ds:(IdType), da:(IdKndType), X:Interface(ds;da;A), es:ES.
es-decl(es;ds;da)
 (e:E. (e  [[interface-compose(f;X)]]) = ((e  [[X]])  can-apply(f;[[X]](e)))  ) 

latex

Definitions	e  X, [[X]], Knd, Id, SQType(T), {T}, s ~ t, <a, b>, Top, , p  q, can-apply(f;x), X(e), AbsInterface(A), E, t.1, es-decl(es;ds;da), ES, Interface(ds;da;A), a:A fp B(a), Type, left + right, Unit, P  Q, P & Q, x:A  B(x), A, b, s = t, , x:A. B(x), P  Q, t  T, x:AB(x)
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-interface-val wf, can-apply wf, band wf, abs-interface wf, can-apply-compose-sq, abs-interface-compose